Nuprl Lemma : sum_shift_q
11,40
postcript
pdf
a
,
b
:
. (
a
b
)
(
E
:({
a
..
b
}
),
k
:
.
a
j
<
b
.
E
(
j
) =
a
+
k
j
<
b
+
k
.
E
(
j
-
k
)
)
latex
Definitions
t
T
,
t
.1
,
CRng
,
<
+*>
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
sum
shift
origin
a, b:
. (a 
b) 
(E:({a..b
}
), k:. 
a j < b. E(j) = a+k j < b+k. E(j - k) 
) a, b:. (a b) (E:({a..b}), k:. a j < b. E(j) = a+k j < b+k. E(j - k) ) T+*>x:A. B(x)a j < b. E(j)